BoundedSizeNoMatch.agda:8,1-9,26
Termination checking failed for the following functions:
  T
Problematic calls:
  T j
    (at BoundedSizeNoMatch.agda:9,23-24)
